es:ES, A:Type, i:Id, ds:x:Id fp Type, conds:k:Knd fp V:Type  (State(ds)V(A + Top)).
es-triggers-params-consistent(es;A;i;ds;conds)   

latex

Definitions	ES, t  T, Type, Id, x. t(x), x:A. B(x), a:A fp B(a), Knd, Top, left + right, x:AB(x), State(ds), x:A  B(x), x.A(x), state@i, P  Q, kind(e), f(x), t.1, valtype(e), KindDeq, x  dom(f), b, , loc(e), s = t, E, P & Q, hasloc(k;i), es-triggers-params-consistent(es;A;i;ds;conds)
Lemmas	hasloc wf, es-E wf, es-loc wf, assert wf, fpf-dom wf, Kind-deq wf, es-kind wf, es-valtype wf, pi1 wf, fpf-ap wf, subtype rel wf, es-state wf, fpf-trivial-subtype-top, decl-state wf, top wf, Knd wf, fpf wf, Id wf, event system wf